Skip to content
Snippets Groups Projects
Commit a0820cd9 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

files generated by tests go in result/ subdir, no oracle ending in .log

parent eb9c757e
No related branches found
No related tags found
No related merge requests found
/* run.config
NOFRAMAC:
EXECNOW: LOG @PTEST_NAME@.res.0.log BIN @PTEST_NAME@.sav @frama-c@ -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya @PTEST_FILE@ -save @PTEST_DIR@/result/@PTEST_NAME@.sav > @PTEST_DIR@/result/@PTEST_NAME@.res.0.log
EXECNOW: LOG @PTEST_NAME@.res.1.log @frama-c@ -load @PTEST_DIR@/result/@PTEST_NAME@.sav -then-on aorai -eva > @PTEST_DIR@/result/@PTEST_NAME@.res.1.log
EXECNOW: LOG @PTEST_NAME@.res.0.log.txt BIN @PTEST_NAME@.sav @frama-c@ -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya @PTEST_FILE@ -save @PTEST_DIR@/result/@PTEST_NAME@.sav > @PTEST_DIR@/result/@PTEST_NAME@.res.0.log.txt
EXECNOW: LOG @PTEST_NAME@.res.1.log.txt @frama-c@ -load @PTEST_DIR@/result/@PTEST_NAME@.sav -then-on aorai -eva > @PTEST_DIR@/result/@PTEST_NAME@.res.1.log.txt
*/
/* run.config_prove
DONTRUN:
......
/* run.config
STDOPT: +"-lib-entry -main g -pdg -pdg-dot tests/pdg/call "
STDOPT: +"-lib-entry -main g -pdg -pdg-dot tests/pdg/result/call "
*/
/* Ne pas modifier : exemple utilisé dans le rapport. */
......
/* run.config
STDOPT: +"-lib-entry -main g -fct-pdg g -pdg-dot tests/pdg/doc"
STDOPT: +"-lib-entry -main g -fct-pdg g -pdg-dot tests/pdg/result/doc"
*/
/* To build the svg file:
* dot -Tsvg tests/pdg/doc.g.dot > tests/pdg/doc.g.svg
* dot -Tsvg tests/pdg/result/doc.g.dot > tests/pdg/result/doc.g.svg
*/
int G1, G2, T[10];
......
......@@ -23,7 +23,7 @@ let main _ =
let kf = Globals.Functions.find_def_by_name "main" in
let pdg = !Db.Pdg.get kf in
Format.printf "%a@." (!Db.Pdg.pretty ~bw:false) pdg;
!Db.Pdg.extract pdg "tests/pdg/dyn_dpds_0.dot";
!Db.Pdg.extract pdg "tests/pdg/result/dyn_dpds_0.dot";
let assert_sid = 5 in (* assert ( *p>G) *)
let assert_stmt, kf = Kernel_function.find_from_sid assert_sid in
let _assert_node =
......@@ -44,6 +44,6 @@ let main _ =
Format.printf "Warning : cannot select %a in this function...@\n"
Locations.Zone.pretty undef;
Format.printf "%a@." (!Db.Pdg.pretty ~bw:false) pdg;
!Db.Pdg.extract pdg "tests/pdg/dyn_dpds_1.dot"
!Db.Pdg.extract pdg "tests/pdg/result/dyn_dpds_1.dot"
let () = Db.Main.extend main
......@@ -22,12 +22,12 @@
[eva] done for function g
[pdg] computing for function f
[pdg] done for function f
[pdg] dot file generated in tests/pdg/call.f.dot
[pdg] dot file generated in tests/pdg/result/call.f.dot
[pdg] computing for function g
[from] Computing for function f
[from] Done for function f
[pdg] done for function g
[pdg] dot file generated in tests/pdg/call.g.dot
[pdg] dot file generated in tests/pdg/result/call.g.dot
[pdg] ====== PDG GRAPH COMPUTED ======
[pdg] PDG for f
{n1}: InCtrl
......
......@@ -16,7 +16,7 @@
[from] Computing for function f
[from] Done for function f
[pdg] done for function g
[pdg] dot file generated in tests/pdg/doc.g.dot
[pdg] dot file generated in tests/pdg/result/doc.g.dot
[pdg] PDG for g
{n1}: InCtrl
{n2}: VarDecl : x
......
......@@ -94,7 +94,7 @@ RESULT for main:
-[--d]-> 13
{n16}: OutRet
-[--d]-> 15
[pdg] dot file generated in tests/pdg/dyn_dpds_0.dot
[pdg] dot file generated in tests/pdg/result/dyn_dpds_0.dot
Warning : cannot select G in this function...
RESULT for main:
{n1}: InCtrl
......@@ -142,4 +142,4 @@ RESULT for main:
-[--d]-> 13
{n16}: OutRet
-[--d]-> 15
[pdg] dot file generated in tests/pdg/dyn_dpds_1.dot
[pdg] dot file generated in tests/pdg/result/dyn_dpds_1.dot
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment