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

[tests] update test for #840 and set oracle

parent 4b7ec708
No related branches found
No related tags found
No related merge requests found
/* run.config* /* run.config*
OPT: -slice-pragma main OPT: -slice-pragma main -then-last -print
*/ */
int g(int x) { return x; } int g(int x) { return x; }
......
[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;
}
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