Commit f18cfe09 authored by Julien Signoles's avatar Julien Signoles
Browse files

[e-acsl] new option -e-acsl to run the plug-in

parent d8fea386
......@@ -78,9 +78,10 @@ let generate_code =
generate_code
let main () =
let s = Options.Project_name.get () in
if s = "" then begin if Options.Check.get () then fail_check () end
else ignore (generate_code s)
if Options.Run.get () then
ignore (generate_code (Options.Project_name.get ()))
else
if Options.Check.get () then fail_check ()
let () = Db.Main.extend main
......
......@@ -36,13 +36,24 @@ module Check =
let kind = `Correctness
end)
module Run =
False
(struct
let option_name = "-e-acsl"
let help = "generate a new project where E-ACSL annotations are \
translated to executable C code"
let kind = `Correctness
let arg_name = "prj"
end)
module Project_name =
EmptyString
String
(struct
let option_name = "-e-acsl-project"
let help = "generate a new project <prj> from the C program where E-ACSL \
code is transformed to C code for runtime assertion checking"
let help = "the name of the generated project is <prj> \
(default to \"e-acsl\")"
let kind = `Correctness
let default = "e-acsl"
let arg_name = "prj"
end)
......
......@@ -24,6 +24,7 @@ open Plugin
include S (** implementation of Log.S for E-ACSL *)
module Check: Bool
module Run: Bool
module Project_name: String
module Use_assert: Bool
......
/* run.config
COMMENT: addrOf
EXECNOW: LOG gen_addrOf.c BIN gen_addrOf.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/addrOf.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_addrOf.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_addrOf.out ./tests/e-acsl-runtime/result/gen_addrOf.c && ./tests/e-acsl-runtime/result/gen_addrOf.out
EXECNOW: LOG gen_addrOf.c BIN gen_addrOf.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/addrOf.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_addrOf.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_addrOf.out ./tests/e-acsl-runtime/result/gen_addrOf.c && ./tests/e-acsl-runtime/result/gen_addrOf.out
*/
int main(void) {
int x = 0;
......
/* run.config
COMMENT: arithmetic operations
COMMENT: add the last assertion when fixing BTS #751
EXECNOW: LOG gen_arith.c BIN gen_arith.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/arith.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_arith.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_arith.out ./tests/e-acsl-runtime/result/gen_arith.c -lgmp && ./tests/e-acsl-runtime/result/gen_arith.out
EXECNOW: LOG gen_arith.c BIN gen_arith.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/arith.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_arith.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_arith.out ./tests/e-acsl-runtime/result/gen_arith.c -lgmp && ./tests/e-acsl-runtime/result/gen_arith.out
*/
int main(void) {
......
/* run.config
COMMENT: arrays
EXECNOW: LOG gen_array.c BIN gen_array.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/array.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_array.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_array.out ./tests/e-acsl-runtime/result/gen_array.c -lgmp && ./tests/e-acsl-runtime/result/gen_array.out
EXECNOW: LOG gen_array.c BIN gen_array.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/array.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_array.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_array.out ./tests/e-acsl-runtime/result/gen_array.c -lgmp && ./tests/e-acsl-runtime/result/gen_array.out
*/
int T1[3],T2[4];
......
/* run.config
COMMENT: \at
EXECNOW: LOG gen_at.c BIN gen_at.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/at.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_at.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_at.out ./tests/e-acsl-runtime/result/gen_at.c -lgmp && ./tests/e-acsl-runtime/result/gen_at.out
EXECNOW: LOG gen_at.c BIN gen_at.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/at.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_at.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_at.out ./tests/e-acsl-runtime/result/gen_at.c -lgmp && ./tests/e-acsl-runtime/result/gen_at.out
*/
int A = 0;
......
/* run.config
COMMENT: cast
EXECNOW: LOG gen_cast.c BIN gen_cast.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/cast.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_cast.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_cast.out ./tests/e-acsl-runtime/result/gen_cast.c -lgmp && ./tests/e-acsl-runtime/result/gen_cast.out
EXECNOW: LOG gen_cast.c BIN gen_cast.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/cast.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_cast.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_cast.out ./tests/e-acsl-runtime/result/gen_cast.c -lgmp && ./tests/e-acsl-runtime/result/gen_cast.out
*/
int main(void) {
......
/* run.config
COMMENT: comparison operators
EXECNOW: LOG gen_comparison.c BIN gen_comparison.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/comparison.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_comparison.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_comparison.out ./tests/e-acsl-runtime/result/gen_comparison.c -lgmp && ./tests/e-acsl-runtime/result/gen_comparison.out
EXECNOW: LOG gen_comparison.c BIN gen_comparison.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/comparison.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_comparison.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_comparison.out ./tests/e-acsl-runtime/result/gen_comparison.c -lgmp && ./tests/e-acsl-runtime/result/gen_comparison.out
*/
int main(void) {
......
/* run.config
COMMENT: empty file
OPT: -e-acsl-check -e-acsl-project p -then-on p -print
OPT: -e-acsl-check -e-acsl -then-on e-acsl -print
*/
/* run.config
COMMENT: assert \false
EXECNOW: LOG gen_false.c BIN gen_false.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/false.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_false.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_false.out ./tests/e-acsl-runtime/result/gen_false.c && ./tests/e-acsl-runtime/result/gen_false.out
EXECNOW: LOG gen_false.c BIN gen_false.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/false.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_false.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_false.out ./tests/e-acsl-runtime/result/gen_false.c && ./tests/e-acsl-runtime/result/gen_false.out
*/
int main(void) {
int x = 0;
......
/* run.config
COMMENT: function contract
EXECNOW: LOG gen_function_contract.c BIN gen_function_contract.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/function_contract.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_function_contract.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_function_contract.out ./tests/e-acsl-runtime/result/gen_function_contract.c -lgmp && ./tests/e-acsl-runtime/result/gen_function_contract.out
EXECNOW: LOG gen_function_contract.c BIN gen_function_contract.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/function_contract.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_function_contract.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_function_contract.out ./tests/e-acsl-runtime/result/gen_function_contract.c -lgmp && ./tests/e-acsl-runtime/result/gen_function_contract.out
*/
int X = 0, Y = 2;
......
/* run.config
COMMENT: integer constant + a stmt after the assertion
COMMENT: waiting for fixing BTS #745
EXECNOW: LOG gen_integer_constant.c BIN gen_integer_constant.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/integer_constant.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_integer_constant.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_integer_constant.out ./tests/e-acsl-runtime/result/gen_integer_constant.c -lgmp && ./tests/e-acsl-runtime/result/gen_integer_constant.out
EXECNOW: LOG gen_integer_constant.c BIN gen_integer_constant.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/integer_constant.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_integer_constant.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_integer_constant.out ./tests/e-acsl-runtime/result/gen_integer_constant.c -lgmp && ./tests/e-acsl-runtime/result/gen_integer_constant.out
*/
int main(void) {
int x;
......
/* run.config
COMMENT: predicate using lazy operators
EXECNOW: LOG gen_lazy.c BIN gen_lazy.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/lazy.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_lazy.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_lazy.out ./tests/e-acsl-runtime/result/gen_lazy.c -lgmp 2> /dev/null && ./tests/e-acsl-runtime/result/gen_lazy.out
EXECNOW: LOG gen_lazy.c BIN gen_lazy.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/lazy.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_lazy.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_lazy.out ./tests/e-acsl-runtime/result/gen_lazy.c -lgmp 2> /dev/null && ./tests/e-acsl-runtime/result/gen_lazy.out
*/
int main(void) {
......
/* run.config
COMMENT: structured stmt with several code annotations inside
EXECNOW: LOG gen_nested_code_annot.c BIN gen_nested_code_annot.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/nested_code_annot.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_nested_code_annot.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_nested_code_annot.out ./tests/e-acsl-runtime/result/gen_nested_code_annot.c -lgmp && ./tests/e-acsl-runtime/result/gen_nested_code_annot.out
EXECNOW: LOG gen_nested_code_annot.c BIN gen_nested_code_annot.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/nested_code_annot.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_nested_code_annot.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_nested_code_annot.out ./tests/e-acsl-runtime/result/gen_nested_code_annot.c -lgmp && ./tests/e-acsl-runtime/result/gen_nested_code_annot.out
*/
int main(void) {
......
/* run.config
COMMENT: predicate [!p]
EXECNOW: LOG gen_not.c BIN gen_not.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/not.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_not.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_not.out ./tests/e-acsl-runtime/result/gen_not.c && ./tests/e-acsl-runtime/result/gen_not.out
EXECNOW: LOG gen_not.c BIN gen_not.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/not.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_not.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_not.out ./tests/e-acsl-runtime/result/gen_not.c && ./tests/e-acsl-runtime/result/gen_not.out
*/
int main(void) {
int x = 0;
......
/* run.config
COMMENT: assert \null == 0
EXECNOW: LOG gen_null.c BIN gen_null.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/null.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_null.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_null.out ./tests/e-acsl-runtime/result/gen_null.c -lgmp && ./tests/e-acsl-runtime/result/gen_null.out
EXECNOW: LOG gen_null.c BIN gen_null.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/null.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_null.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_null.out ./tests/e-acsl-runtime/result/gen_null.c -lgmp && ./tests/e-acsl-runtime/result/gen_null.out
*/
int main(void) {
......
/* run.config
COMMENT: non integer constants
EXECNOW: LOG gen_other_constants.c BIN gen_other_constants.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/other_constants.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_other_constants.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_other_constants.out ./tests/e-acsl-runtime/result/gen_other_constants.c -lgmp && ./tests/e-acsl-runtime/result/gen_other_constants.out
EXECNOW: LOG gen_other_constants.c BIN gen_other_constants.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/other_constants.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_other_constants.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_other_constants.out ./tests/e-acsl-runtime/result/gen_other_constants.c -lgmp && ./tests/e-acsl-runtime/result/gen_other_constants.out
*/
enum bool { false, true };
......
/* run.config
COMMENT: pointers and pointer arithmetic
EXECNOW: LOG gen_ptr.c BIN gen_ptr.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/ptr.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_ptr.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_ptr.out ./tests/e-acsl-runtime/result/gen_ptr.c -lgmp && ./tests/e-acsl-runtime/result/gen_ptr.out
EXECNOW: LOG gen_ptr.c BIN gen_ptr.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/ptr.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_ptr.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_ptr.out ./tests/e-acsl-runtime/result/gen_ptr.c -lgmp && ./tests/e-acsl-runtime/result/gen_ptr.out
*/
int main(void) {
......
/* run.config
COMMENT: \result
EXECNOW: LOG gen_result.c BIN gen_result.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/result.i -e-acsl-project p -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_result.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_result.out ./tests/e-acsl-runtime/result/gen_result.c -lgmp && ./tests/e-acsl-runtime/result/gen_result.out
EXECNOW: LOG gen_result.c BIN gen_result.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/result.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_result.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_result.out ./tests/e-acsl-runtime/result/gen_result.c -lgmp && ./tests/e-acsl-runtime/result/gen_result.out
*/
/*@ ensures \result == (int)(x - x); */
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment