Merge branch 'feature/basile/eacsl-99-logical-arrays' into 'master'
[eacsl] Add support for logical array comparison in E-ACSL Closes e-acsl#99 See merge request frama-c/frama-c!2704
Showing
- src/plugins/e-acsl/Makefile.in 1 addition, 0 deletionssrc/plugins/e-acsl/Makefile.in
- src/plugins/e-acsl/doc/Changelog 2 additions, 0 deletionssrc/plugins/e-acsl/doc/Changelog
- src/plugins/e-acsl/doc/refman/changes_modern.tex 1 addition, 0 deletionssrc/plugins/e-acsl/doc/refman/changes_modern.tex
- src/plugins/e-acsl/doc/refman/speclang_modern.tex 10 additions, 1 deletionsrc/plugins/e-acsl/doc/refman/speclang_modern.tex
- src/plugins/e-acsl/headers/header_spec.txt 2 additions, 0 deletionssrc/plugins/e-acsl/headers/header_spec.txt
- src/plugins/e-acsl/src/code_generator/at_with_lscope.ml 6 additions, 6 deletionssrc/plugins/e-acsl/src/code_generator/at_with_lscope.ml
- src/plugins/e-acsl/src/code_generator/constructor.ml 34 additions, 2 deletionssrc/plugins/e-acsl/src/code_generator/constructor.ml
- src/plugins/e-acsl/src/code_generator/constructor.mli 41 additions, 0 deletionssrc/plugins/e-acsl/src/code_generator/constructor.mli
- src/plugins/e-acsl/src/code_generator/env.ml 18 additions, 3 deletionssrc/plugins/e-acsl/src/code_generator/env.ml
- src/plugins/e-acsl/src/code_generator/env.mli 9 additions, 0 deletionssrc/plugins/e-acsl/src/code_generator/env.mli
- src/plugins/e-acsl/src/code_generator/global_observer.ml 11 additions, 7 deletionssrc/plugins/e-acsl/src/code_generator/global_observer.ml
- src/plugins/e-acsl/src/code_generator/gmp.ml 2 additions, 2 deletionssrc/plugins/e-acsl/src/code_generator/gmp.ml
- src/plugins/e-acsl/src/code_generator/logic_array.ml 294 additions, 0 deletionssrc/plugins/e-acsl/src/code_generator/logic_array.ml
- src/plugins/e-acsl/src/code_generator/logic_array.mli 42 additions, 0 deletionssrc/plugins/e-acsl/src/code_generator/logic_array.mli
- src/plugins/e-acsl/src/code_generator/logic_functions.ml 1 addition, 1 deletionsrc/plugins/e-acsl/src/code_generator/logic_functions.ml
- src/plugins/e-acsl/src/code_generator/loops.ml 8 additions, 10 deletionssrc/plugins/e-acsl/src/code_generator/loops.ml
- src/plugins/e-acsl/src/code_generator/mmodel_translate.ml 45 additions, 62 deletionssrc/plugins/e-acsl/src/code_generator/mmodel_translate.ml
- src/plugins/e-acsl/src/code_generator/quantif.ml 7 additions, 8 deletionssrc/plugins/e-acsl/src/code_generator/quantif.ml
- src/plugins/e-acsl/src/code_generator/rational.ml 4 additions, 5 deletionssrc/plugins/e-acsl/src/code_generator/rational.ml
- src/plugins/e-acsl/src/code_generator/temporal.ml 1 addition, 1 deletionsrc/plugins/e-acsl/src/code_generator/temporal.ml
Loading
Please register or sign in to comment