Commit 7963a679 authored by POLLIEN Baptiste's avatar POLLIEN Baptiste
Browse files

Working script

parent 48d09cbb
(* Frama-C journal generated at 10:20 the 25/02/2021 *)
(* Frama-C journal generated at 13:47 the 02/03/2021 *)
exception Unreachable
exception Exception of string
......@@ -7,11 +7,14 @@ exception Exception of string
(* Run the user commands *)
let run () =
Dynamic.Parameter.String.set "-wp-fct" "@default,int32_quat_integrate_fi";
Dynamic.Parameter.Bool.set "-eva" true;
Dynamic.Parameter.Bool.set "-lib-entry" true;
Dynamic.Parameter.String.set "-main" "int32_quat_of_rmat";
Dynamic.Parameter.Bool.set "-wp" true;
Dynamic.Parameter.String.set "-wp-cache" "update";
Dynamic.Parameter.String.set "-wp-model" "@default,real+Cast";
Dynamic.Parameter.String.set "-wp-prover"
"@default,alt-ergo,z3-ce,cvc4-strings-ce,tip";
"@default,alt-ergo,cvc4-strings-ce,tip";
Dynamic.Parameter.Bool.set "-rte" true;
Dynamic.Parameter.String.set "-cpp-extra-args" "-I../include";
Dynamic.Parameter.String.set "-cpp-extra-args"
......@@ -20,6 +23,7 @@ let run () =
"/home/disc/b.pollien/Documents/paparazzi/sw/airborne/math/pprz_algebra_int.c";
File.init_from_cmdline ();
!Db.RteGen.compute ();
!Db.Value.compute ();
Project.clear
~selection:(State_selection.of_list
[ State.get "Report.print_once";
......@@ -1164,6 +1168,33 @@ let run () =
State.get "Property_status.Consolidated_status";
State.get "Consolidation graph" ])
();
Dynamic.Parameter.Bool.clear "-wp" ();
Project.set_keep_current false;
let __ = Callgraph.Cg.get () in
let __ = Callgraph.Cg.get () in
let __ = Callgraph.Cg.get () in
let __ = Callgraph.Cg.get () in
let __ = Callgraph.Cg.get () in
let __ = Callgraph.Cg.get () in
let __ = Callgraph.Cg.get () in
let __ = Callgraph.Cg.get () in
let __ = Callgraph.Cg.get () in
let __ = Callgraph.Cg.get () in
let __ = Callgraph.Cg.get () in
let __ = Callgraph.Cg.get () in
let __ = Callgraph.Cg.get () in
let __ = Callgraph.Cg.get () in
let __ = Callgraph.Cg.get () in
let __ = Callgraph.Cg.get () in
let __ = Callgraph.Cg.get () in
let __ = Callgraph.Cg.get () in
let __ = Callgraph.Cg.get () in
let __ = Callgraph.Cg.get () in
let __ = Callgraph.Cg.get () in
let __ = Callgraph.Cg.get () in
let __ = Callgraph.Cg.get () in
let __ = Callgraph.Cg.get () in
let __ = Callgraph.Cg.get () in
Project.clear
~selection:(State_selection.of_list
[ State.get "Report.print_once";
......@@ -1292,168 +1323,6 @@ let run () =
State.get "Property_status.Consolidated_status";
State.get "Consolidation graph" ])
();
Project.clear
~selection:(State_selection.of_list
[ State.get "Report.print_once";
State.get "Report.print_csv_once";
State.get "Report.classify_once";
State.get "Property_status.Consolidated_status";
State.get "Consolidation graph" ])
();
Project.clear
~selection:(State_selection.of_list
[ State.get "Report.print_once";
State.get "Report.print_csv_once";
State.get "Report.classify_once";
State.get "Property_status.Consolidated_status";
State.get "Consolidation graph" ])
();
Project.clear
~selection:(State_selection.of_list
[ State.get "Report.print_once";
State.get "Report.print_csv_once";
State.get "Report.classify_once";
State.get "Property_status.Consolidated_status";
State.get "Consolidation graph" ])
();
Project.clear
~selection:(State_selection.of_list
[ State.get "Report.print_once";
State.get "Report.print_csv_once";
State.get "Report.classify_once";
State.get "Property_status.Consolidated_status";
State.get "Consolidation graph" ])
();
Project.clear
~selection:(State_selection.of_list
[ State.get "Report.print_once";
State.get "Report.print_csv_once";
State.get "Report.classify_once";
State.get "Property_status.Consolidated_status";
State.get "Consolidation graph" ])
();
Project.clear
~selection:(State_selection.of_list
[ State.get "Report.print_once";
State.get "Report.print_csv_once";
State.get "Report.classify_once";
State.get "Property_status.Consolidated_status";
State.get "Consolidation graph" ])
();
Project.clear
~selection:(State_selection.of_list
[ State.get "Report.print_once";
State.get "Report.print_csv_once";
State.get "Report.classify_once";
State.get "Property_status.Consolidated_status";
State.get "Consolidation graph" ])
();
Project.clear
~selection:(State_selection.of_list
[ State.get "Report.print_once";
State.get "Report.print_csv_once";
State.get "Report.classify_once";
State.get "Property_status.Consolidated_status";
State.get "Consolidation graph" ])
();
Project.clear
~selection:(State_selection.of_list
[ State.get "Report.print_once";
State.get "Report.print_csv_once";
State.get "Report.classify_once";
State.get "Property_status.Consolidated_status";
State.get "Consolidation graph" ])
();
Project.clear
~selection:(State_selection.of_list
[ State.get "Report.print_once";
State.get "Report.print_csv_once";
State.get "Report.classify_once";
State.get "Property_status.Consolidated_status";
State.get "Consolidation graph" ])
();
Project.clear
~selection:(State_selection.of_list
[ State.get "Report.print_once";
State.get "Report.print_csv_once";
State.get "Report.classify_once";
State.get "Property_status.Consolidated_status";
State.get "Consolidation graph" ])
();
Project.clear
~selection:(State_selection.of_list
[ State.get "Report.print_once";
State.get "Report.print_csv_once";
State.get "Report.classify_once";
State.get "Property_status.Consolidated_status";
State.get "Consolidation graph" ])
();
Project.clear
~selection:(State_selection.of_list
[ State.get "Report.print_once";
State.get "Report.print_csv_once";
State.get "Report.classify_once";
State.get "Property_status.Consolidated_status";
State.get "Consolidation graph" ])
();
Project.clear
~selection:(State_selection.of_list
[ State.get "Report.print_once";
State.get "Report.print_csv_once";
State.get "Report.classify_once";
State.get "Property_status.Consolidated_status";
State.get "Consolidation graph" ])
();
Project.clear
~selection:(State_selection.of_list
[ State.get "Report.print_once";
State.get "Report.print_csv_once";
State.get "Report.classify_once";
State.get "Property_status.Consolidated_status";
State.get "Consolidation graph" ])
();
Project.clear
~selection:(State_selection.of_list
[ State.get "Report.print_once";
State.get "Report.print_csv_once";
State.get "Report.classify_once";
State.get "Property_status.Consolidated_status";
State.get "Consolidation graph" ])
();
Project.clear
~selection:(State_selection.of_list
[ State.get "Report.print_once";
State.get "Report.print_csv_once";
State.get "Report.classify_once";
State.get "Property_status.Consolidated_status";
State.get "Consolidation graph" ])
();
Project.clear
~selection:(State_selection.of_list
[ State.get "Report.print_once";
State.get "Report.print_csv_once";
State.get "Report.classify_once";
State.get "Property_status.Consolidated_status";
State.get "Consolidation graph" ])
();
Project.clear
~selection:(State_selection.of_list
[ State.get "Report.print_once";
State.get "Report.print_csv_once";
State.get "Report.classify_once";
State.get "Property_status.Consolidated_status";
State.get "Consolidation graph" ])
();
Project.clear
~selection:(State_selection.of_list
[ State.get "Report.print_once";
State.get "Report.print_csv_once";
State.get "Report.classify_once";
State.get "Property_status.Consolidated_status";
State.get "Consolidation graph" ])
();
Dynamic.Parameter.String.clear "-wp-fct" ();
Project.set_keep_current false;
()
(* Main *)
......
{ "prover": "Z3:4.8.10:counterexamples", "verdict": "failed" }
{ "prover": "Z3:4.8.10:counterexamples", "verdict": "failed" }
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout", "time": 10. }
{ "prover": "Alt-Ergo:2.3.3", "verdict": "valid", "time": 0.018,
"steps": 97 }
{ "prover": "Alt-Ergo:2.3.3", "verdict": "valid", "time": 0.3837,
"steps": 597 }
{ "prover": "Alt-Ergo:2.3.3", "verdict": "timeout", "time": 10. }
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 0.05 }
{ "prover": "Alt-Ergo:2.3.3", "verdict": "timeout", "time": 10. }
{ "prover": "Alt-Ergo:2.3.3", "verdict": "timeout", "time": 10. }
{ "prover": "Alt-Ergo:2.3.3", "verdict": "timeout", "time": 10. }
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout", "time": 10. }
{ "prover": "Alt-Ergo:2.3.3", "verdict": "valid", "time": 0.0087,
"steps": 22 }
{ "prover": "Alt-Ergo:2.3.3", "verdict": "valid", "time": 0.0111,
"steps": 12 }
{ "prover": "Alt-Ergo:2.3.3", "verdict": "valid", "time": 0.0804,
"steps": 278 }
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 0.14 }
{ "prover": "Alt-Ergo:2.3.3", "verdict": "timeout", "time": 10. }
{ "prover": "Alt-Ergo:2.3.3", "verdict": "timeout", "time": 10. }
{ "prover": "Alt-Ergo:2.3.3", "verdict": "timeout", "time": 10. }
{ "prover": "Alt-Ergo:2.3.3", "verdict": "timeout", "time": 10. }
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