diff --git a/tests/slicing/function_lvar.i b/tests/slicing/function_lvar.i index c7d245c4528e1d6da3729f54cae149cd9ec4d47e..05cc5c69a2033223a3a35a16e22ba0b9b2558b4f 100644 --- a/tests/slicing/function_lvar.i +++ b/tests/slicing/function_lvar.i @@ -1,5 +1,5 @@ /* run.config* -OPT: -slice-pragma main +OPT: -slice-pragma main -then-last -print */ int g(int x) { return x; } diff --git a/tests/slicing/oracle/function_lvar.res.oracle b/tests/slicing/oracle/function_lvar.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..667a53c29a9dadfe352bca9c7caf5212f03e305d --- /dev/null +++ b/tests/slicing/oracle/function_lvar.res.oracle @@ -0,0 +1,57 @@ +[kernel] Parsing tests/slicing/function_lvar.i (no preprocessing) +[slicing] slicing requests in progress... +[eva] Analyzing a complete application starting at main +[eva] Computing initial state +[eva] Initial state computed +[eva:initial-state] Values of globals at initialization + +[eva] done for function main +[eva:summary] ====== ANALYSIS SUMMARY ====== + ---------------------------------------------------------------------------- + 2 functions analyzed (out of 2): 100% coverage. + In these functions, 5 statements reached (out of 5): 100% coverage. + ---------------------------------------------------------------------------- + No errors or warnings raised during the analysis. + ---------------------------------------------------------------------------- + 0 alarms generated by the analysis. + ---------------------------------------------------------------------------- + Evaluation of the logical properties reached by the analysis: + Assertions 1 valid 0 unknown 0 invalid 1 total + Preconditions 0 valid 0 unknown 0 invalid 0 total + 100% of the logical properties reached have been proven. + ---------------------------------------------------------------------------- +[slicing] initializing slicing ... +[slicing] interpreting slicing requests from the command line... +[pdg] computing for function main +[from] Computing for function g +[from] Done for function g +[pdg] done for function main +[slicing] applying all slicing requests... +[slicing] applying 0 actions... +[slicing] applying all slicing requests... +[slicing] applying 1 actions... +[slicing] applying actions: 1/1... +[pdg] computing for function g +[pdg] done for function g +[slicing] exporting project to 'Slicing export'... +[slicing] applying all slicing requests... +[slicing] applying 0 actions... +[sparecode] remove unused global declarations from project 'Slicing export tmp' +[sparecode] removed unused global declarations in new project 'Slicing export' +/* Generated by Frama-C */ +int g(int x); + +void g_slice_1(void) +{ + return; +} + +void main(void) +{ + /*@ assert &g 鈮� &g; */ ; + /*@ slice pragma stmt; */ + g_slice_1(); + return; +} + +