Revision 6a93d814
Added by Xavier Thirioux almost 10 years ago
- added
- modified
- copied
- renamed
- deleted
- optim
- .frama-c
- StreamsLib.glob
- StreamsLib.v
- StreamsLib.vo
- TODO.org
- clocks7
- lustre.glob
- lustre.v
- oversampling
- .frama-c
- out
- typed
- Axiomatic.v
- Axiomatic.vo
- Compound.v
- Compound.vo
- Globals.v
- Globals.vo
- S__arrow_mem_pack.v
- S__arrow_mem_pack.vo
- S__arrow_reg.v
- S__arrow_reg.vo
- S_f_mem_pack.v
- S_f_mem_pack.vo
- S_f_reg.v
- S_f_reg.vo
- S_g_mem_pack.v
- S_g_mem_pack.vo
- S_g_reg.v
- S_g_reg.vo
- f_reset_post.coq
- f_reset_post_Coq.v
- f_reset_post_Coq_Coq.out
- f_step_assert.coq
- f_step_assert_2.coq
- f_step_assert_2_Coq.v
- f_step_assert_2_Coq_Coq.out
- f_step_assert_3.coq
- f_step_assert_3_Coq.v
- f_step_assert_3_Coq_Coq.out
- f_step_assert_4.coq
- f_step_assert_4_Coq.v
- f_step_assert_4_Coq_Coq.out
- f_step_assert_5.coq
- f_step_assert_5_Coq.v
- f_step_assert_5_Coq_Coq.out
- f_step_assert_6.coq
- f_step_assert_6_Coq.v
- f_step_assert_6_Coq_Coq.out
- f_step_assert_Coq.v
- f_step_assert_Coq.vo
- f_step_post.coq
- f_step_post_Coq.v
- f_step_post_Coq.vo
- g_reset_call_f_reset_pre.coq
- g_reset_call_f_reset_pre_Coq.v
- g_reset_call_f_reset_pre_Coq_Coq.out
- g_reset_post.coq
- g_reset_post_Coq.v
- g_reset_post_Coq_Coq.out
- g_step_assert.coq
- g_step_assert_2.coq
- g_step_assert_2_Coq.v
- g_step_assert_2_Coq_Coq.out
- g_step_assert_3.coq
- g_step_assert_3_Coq.v
- g_step_assert_3_Coq_Coq.out
- g_step_assert_4.coq
- g_step_assert_4_Coq.v
- g_step_assert_4_Coq_Coq.out
- g_step_assert_5.coq
- g_step_assert_5_Coq.v
- g_step_assert_5_Coq_Coq.out
- g_step_assert_6.coq
- g_step_assert_6_Coq.v
- g_step_assert_6_Coq_Coq.out
- g_step_assert_7.coq
- g_step_assert_7_Coq.v
- g_step_assert_7_Coq_Coq.out
- g_step_assert_Coq.v
- g_step_assert_Coq.vo
- g_step_call_f_step_pre.coq
- g_step_call_f_step_pre_4.coq
- g_step_call_f_step_pre_4_Coq.v
- g_step_call_f_step_pre_Coq.v
- g_step_post.coq
- g_step_post_Coq.v
- g_step_post_Coq.vo
- typed
- oversampling0.c
- oversampling0.h
- oversampling0.lus
- oversampling0_1.c
- oversampling0_2.c
- oversampling0_3.c
- oversampling0_4.c
- oversampling0_alloc.h
- oversampling0_denot.h
- streams2_lus.v
- streams_acsl.c
- streams_acsl.h
- streams_acsl_2.h
- streams_acsl_3.h
- streams_lus.v
- wp0.script
- wp1.script
- wp2.script
- wp3.script
- wp4.script
- wp5.script
- wp6.script
- wp7.script
- wp8.script
- wp9.script
- streams2_lus.v
- wpdir
- typed
- Axiomatic.ergo
- toto_step_assert.ergo
- toto_step_assert_11.ergo
- toto_step_assert_11_Alt-Ergo.mlw
- toto_step_assert_11_Alt-Ergo.out
- toto_step_assert_12.ergo
- toto_step_assert_12_Alt-Ergo.mlw
- toto_step_assert_12_Alt-Ergo.out
- toto_step_assert_13.ergo
- toto_step_assert_13_Alt-Ergo.mlw
- toto_step_assert_13_Alt-Ergo.out
- toto_step_assert_14.ergo
- toto_step_assert_14_Alt-Ergo.mlw
- toto_step_assert_14_Alt-Ergo.out
- toto_step_assert_15.ergo
- toto_step_assert_15_Alt-Ergo.mlw
- toto_step_assert_15_Alt-Ergo.out
- toto_step_assert_16.ergo
- toto_step_assert_16_Alt-Ergo.mlw
- toto_step_assert_16_Alt-Ergo.out
- toto_step_assert_17.ergo
- toto_step_assert_17_Alt-Ergo.mlw
- toto_step_assert_17_Alt-Ergo.out
- toto_step_assert_18.ergo
- toto_step_assert_18_Alt-Ergo.mlw
- toto_step_assert_18_Alt-Ergo.out
- toto_step_assert_19.ergo
- toto_step_assert_19_Alt-Ergo.mlw
- toto_step_assert_19_Alt-Ergo.out
- toto_step_assert_2.ergo
- toto_step_assert_20.ergo
- toto_step_assert_20_Alt-Ergo.mlw
- toto_step_assert_20_Alt-Ergo.out
- toto_step_assert_21.ergo
- toto_step_assert_21_Alt-Ergo.mlw
- toto_step_assert_21_Alt-Ergo.out
- toto_step_assert_22.ergo
- toto_step_assert_22_Alt-Ergo.mlw
- toto_step_assert_22_Alt-Ergo.out
- toto_step_assert_23.ergo
- toto_step_assert_23_Alt-Ergo.mlw
- toto_step_assert_23_Alt-Ergo.out
- toto_step_assert_2_Alt-Ergo.mlw
- toto_step_assert_2_Alt-Ergo.out
- toto_step_assert_3.ergo
- toto_step_assert_3_Alt-Ergo.mlw
- toto_step_assert_3_Alt-Ergo.out
- toto_step_assert_4.ergo
- toto_step_assert_4_Alt-Ergo.mlw
- toto_step_assert_4_Alt-Ergo.out
- toto_step_assert_5.ergo
- toto_step_assert_5_Alt-Ergo.mlw
- toto_step_assert_5_Alt-Ergo.out
- toto_step_assert_Alt-Ergo.mlw
- toto_step_assert_Alt-Ergo.out
- typed
- scripts
- tests
added a directory optim/ dedicated to experiments about injecting/proving ACSL spec into optimized programs.