Skip to content
Snippets Groups Projects
Commit b3d0ff2e authored by Andre Maroneze's avatar Andre Maroneze
Browse files

[tests] remove extraneous test oracles

parent c9de08f5
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 0 additions and 405 deletions
src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.res.oracle deleted 100644 → 0
+ 0
− 254
View file @ c9de08f5
# frama-c -wp [...]
[kernel] Parsing tests/wp_hoare/alias_assigns_hypotheses.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function comprehension_alias
------------------------------------------------------------
Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 85) in 'comprehension_alias':
Prove: true.
------------------------------------------------------------
Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 86) in 'comprehension_alias':
Prove: true.
------------------------------------------------------------
Goal Assigns (file tests/wp_hoare/alias_assigns_hypotheses.i, line 84) in 'comprehension_alias':
Effect at line 88
Prove: true.
------------------------------------------------------------
------------------------------------------------------------
Function field_alias
------------------------------------------------------------
Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 54) in 'field_alias':
Prove: true.
------------------------------------------------------------
Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 55) in 'field_alias':
Prove: true.
------------------------------------------------------------
Goal Assigns (file tests/wp_hoare/alias_assigns_hypotheses.i, line 53) in 'field_alias':
Effect at line 57
Prove: true.
------------------------------------------------------------
------------------------------------------------------------
Function field_range_alias
------------------------------------------------------------
Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 66) in 'field_range_alias':
Prove: true.
------------------------------------------------------------
Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 67) in 'field_range_alias':
Prove: true.
------------------------------------------------------------
Goal Assigns (file tests/wp_hoare/alias_assigns_hypotheses.i, line 65) in 'field_range_alias':
Effect at line 69
Prove: true.
------------------------------------------------------------
------------------------------------------------------------
Function formal_alias
------------------------------------------------------------
Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 25) in 'formal_alias':
Prove: true.
------------------------------------------------------------
Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 26) in 'formal_alias':
Prove: true.
------------------------------------------------------------
Goal Assigns (file tests/wp_hoare/alias_assigns_hypotheses.i, line 24) in 'formal_alias':
Effect at line 28
Prove: true.
------------------------------------------------------------
------------------------------------------------------------
Function formal_alias_array
------------------------------------------------------------
Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 40) in 'formal_alias_array':
Prove: true.
------------------------------------------------------------
Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 41) in 'formal_alias_array':
Prove: true.
------------------------------------------------------------
Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 42) in 'formal_alias_array':
Prove: true.
------------------------------------------------------------
Goal Assigns (file tests/wp_hoare/alias_assigns_hypotheses.i, line 39) in 'formal_alias_array' (1/2):
Effect at line 44
Prove: true.
------------------------------------------------------------
Goal Assigns (file tests/wp_hoare/alias_assigns_hypotheses.i, line 39) in 'formal_alias_array' (2/2):
Effect at line 45
Prove: true.
------------------------------------------------------------
------------------------------------------------------------
Function formal_no_alias
------------------------------------------------------------
Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 33) in 'formal_no_alias':
Prove: true.
------------------------------------------------------------
Goal Assigns (file tests/wp_hoare/alias_assigns_hypotheses.i, line 32) in 'formal_no_alias':
Effect at line 35
Prove: true.
------------------------------------------------------------
------------------------------------------------------------
Function global_alias
------------------------------------------------------------
Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 10) in 'global_alias':
Prove: true.
------------------------------------------------------------
Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 11) in 'global_alias':
Prove: true.
------------------------------------------------------------
Goal Assigns (file tests/wp_hoare/alias_assigns_hypotheses.i, line 9) in 'global_alias':
Effect at line 13
Prove: true.
------------------------------------------------------------
------------------------------------------------------------
Function global_no_alias
------------------------------------------------------------
Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 18) in 'global_no_alias':
Prove: true.
------------------------------------------------------------
Goal Assigns (file tests/wp_hoare/alias_assigns_hypotheses.i, line 17) in 'global_no_alias':
Effect at line 20
Prove: true.
------------------------------------------------------------
------------------------------------------------------------
Function set_alias
------------------------------------------------------------
Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 74) in 'set_alias':
Prove: true.
------------------------------------------------------------
Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 75) in 'set_alias':
Prove: true.
------------------------------------------------------------
Goal Assigns (file tests/wp_hoare/alias_assigns_hypotheses.i, line 73) in 'set_alias':
Effect at line 77
Prove: true.
------------------------------------------------------------
------------------------------------------------------------
Function union_alias
------------------------------------------------------------
Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 95) in 'union_alias':
Prove: true.
------------------------------------------------------------
Goal Post-condition (file tests/wp_hoare/alias_assigns_hypotheses.i, line 96) in 'union_alias':
Prove: true.
------------------------------------------------------------
Goal Assigns (file tests/wp_hoare/alias_assigns_hypotheses.i, line 94) in 'union_alias':
Effect at line 98
Prove: true.
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'global_alias':
/*@
behavior typed:
requires \separated(g_alias,\union(&g_alias,global+(..)));
*/
void global_alias(void);
[wp] Warning: Memory model hypotheses for function 'global_no_alias':
/*@ behavior typed: requires \separated(g_alias,&g_alias); */
void global_no_alias(void);
[wp] Warning: Memory model hypotheses for function 'formal_alias':
/*@
behavior typed:
requires \separated(global+(..),f_alias);
requires \separated(f_alias,global+(..));
*/
void formal_alias(int *f_alias);
[wp] Warning: Memory model hypotheses for function 'formal_alias_array':
/*@
behavior typed:
requires \separated(global+(..),alias_array+(..));
requires \separated(&(*alias_array)[0 .. 1],global+(..));
*/
void formal_alias_array(int (*alias_array)[2]);
[wp] Warning: Memory model hypotheses for function 'field_alias':
/*@
behavior typed:
requires \separated(global+(..),x);
requires \separated(&x->x,global+(..));
*/
void field_alias(struct X *x);
[wp] Warning: Memory model hypotheses for function 'field_range_alias':
/*@
behavior typed:
requires \separated(global+(..),x+(..));
requires \separated(&(x + (0 .. 3))->x,global+(..));
*/
void field_range_alias(struct X *x);
[wp] Warning: Memory model hypotheses for function 'set_alias':
/*@
behavior typed:
requires \separated(\union(global+(..),&g_alias),f_alias);
requires \separated({g_alias, f_alias},\union(&g_alias,global+(..)));
*/
void set_alias(int *f_alias);
[wp] Warning: Memory model hypotheses for function 'comprehension_alias':
/*@
behavior typed:
requires \separated({alias | int *alias; alias ≡ \at(g_alias,Pre)},
\union(&g_alias,global+(..)));
*/
void comprehension_alias(void);
[wp] Warning: Memory model hypotheses for function 'union_alias':
/*@
behavior typed:
requires \separated(\union(global+(..),&g_alias),f_alias);
requires \separated({g_alias, f_alias},\union(&g_alias,global+(..)));
*/
void union_alias(int *f_alias);
src/plugins/wp/tests/wp_plugin/oracle/unsigned.err.oracle deleted 100644 → 0
+ 0
− 0
View file @ c9de08f5
src/plugins/wp/tests/wp_plugin/oracle/unsigned.res.oracle deleted 100644 → 0
+ 0
− 18
View file @ c9de08f5
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/unsigned.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] 1 goal scheduled
[wp] [Tactical] Goal typed_lemma_U32 : Valid
[wp] Proved goals: 1 / 1
Qed: 0
Script: 1
------------------------------------------------------------
Global
------------------------------------------------------------
Lemma U32:
Prove: (is_uint32 x_0) -> ((land 4294967295 x_0)=x_0)
Prover Tactical returns Valid
------------------------------------------------------------
src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.0.res.oracle deleted 100644 → 0
+ 0
− 25
View file @ c9de08f5
# frama-c -wp -wp-no-let -wp-timeout 45 -wp-steps 1500 [...]
[kernel] Parsing tests/wp_plugin/bool.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 7 goals scheduled
[wp] [Alt-Ergo 2.0.0] Goal typed_band_bool_false_ensures : Unsuccess
[wp] [Qed] Goal typed_band_bool_true_ensures : Valid
[wp] [Alt-Ergo 2.0.0] Goal typed_bor_bool_false_ensures : Unsuccess
[wp] [Alt-Ergo 2.0.0] Goal typed_bor_bool_true_ensures : Valid
[wp] [Alt-Ergo 2.0.0] Goal typed_bxor_bool_false_ensures : Unsuccess
[wp] [Qed] Goal typed_bxor_bool_true_ensures : Valid
[wp] [Alt-Ergo 2.0.0] Goal typed_job_ensures : Unsuccess
[wp] Proved goals: 3 / 7
Qed: 2
Alt-Ergo 2.0.0: 1 (unsuccess: 4)
[wp] Report in: 'tests/wp_plugin/oracle_qualif/bool.0.report.json'
[wp] Report out: 'tests/wp_plugin/result_qualif/bool.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
job - - 1 0.0%
bor_bool - 1 (4..16) 2 50.0%
band_bool 1 - 2 50.0%
bxor_bool 1 - 2 50.0%
-------------------------------------------------------------
src/plugins/wp/tests/wp_tip/oracle_qualif/induction.res.oracle deleted 100644 → 0
+ 0
− 10
View file @ c9de08f5
# frama-c -wp [...]
[kernel] Parsing tests/wp_tip/induction.i (no preprocessing)
[wp] Running WP plugin...
[wp] 1 goal scheduled
[wp] [Script] Goal typed_lemma_Simple : Unsuccess
[wp] Proved goals: 0 / 1
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
Axiomatic Inductive - - 1 0.0%
------------------------------------------------------------
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.res.oracle deleted 100644 → 0
+ 0
− 22
View file @ c9de08f5
# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...]
[kernel] Parsing tests/wp_typed/user_init.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 8 goals scheduled
[wp] [Alt-Ergo 2.0.0] Goal typed_init_ensures : Valid
[wp] [Alt-Ergo 2.0.0] Goal typed_init_loop_invariant_Partial_preserved : Valid
[wp] [Qed] Goal typed_init_loop_invariant_Partial_established : Valid
[wp] [Alt-Ergo 2.0.0] Goal typed_init_loop_invariant_Range_preserved : Valid
[wp] [Qed] Goal typed_init_loop_invariant_Range_established : Valid
[wp] [Qed] Goal typed_init_loop_assigns_part1 : Valid
[wp] [Alt-Ergo 2.0.0] Goal typed_init_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_init_assigns : Valid
[wp] Proved goals: 8 / 8
Qed: 4
Alt-Ergo 2.0.0: 4
[wp] Report 'tests/wp_typed/user_init.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
init 4 4 (48..60) 8 100%
-------------------------------------------------------------
tests/metrics/oracle/libc.3.res.oracle deleted 100644 → 0
+ 0
− 1
View file @ c9de08f5
[kernel] Parsing tests/metrics/libc.c (with preprocessing)
tests/misc/oracle/log-file.0.res.oracle deleted 100644 → 0
+ 0
− 44
View file @ c9de08f5
[kernel] Parsing tests/misc/log-file.i (no preprocessing)
[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] computing for function f <- main.
Called from tests/misc/log-file.i:20.
[kernel:annot:missing-spec] tests/misc/log-file.i:20: Warning:
Neither code nor specification for function f, generating default assigns from the prototype
[eva] using specification for function f
[eva] Done for function f
[eva] computing for function g <- main.
Called from tests/misc/log-file.i:21.
[eva] using specification for function g
[eva] tests/misc/log-file.i:17: Warning:
no 'assigns \result \from ...' clause specified for function g
[eva] Done for function g
[eva] tests/misc/log-file.i:22: starting to merge loop iterations
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
r ∈ [--..--]
__retres ∈ {0}
[from] Computing for function main
[from] Computing for function f <-main
[from] Done for function f
[from] Computing for function g <-main
[from] Done for function g
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function f:
\result FROM \nothing
[from] Function g:
\result FROM ANYTHING(origin:Unknown)
[from] Function main:
\result FROM \nothing
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main:
r; i; __retres
[inout] Inputs for function main:
\nothing
tests/misc/oracle/log-file.1.res.oracle deleted 100644 → 0
+ 0
− 8
View file @ c9de08f5
[kernel] Parsing tests/misc/log-file.i (no preprocessing)
[kernel:foo-category] result with dkey
[kernel] result
[kernel:foo-category] feedback with dkey
[kernel] feedback
[kernel:foo-category] debug (level 0) with dkey
[kernel] debug (level 0)
[kernel] Warning: warning
tests/misc/oracle/my_visitor.res.oracle deleted 100644 → 0
+ 0
− 23
View file @ c9de08f5
[kernel] Warning: emitter emitter1: correctness parameter -s does not exist anymore. Ignored.
[kernel] Warning: emitter emitter2: correctness parameter -s2 does not exist anymore. Ignored.
[kernel] Warning: 13 states in saved file ignored. They are invalid in this Frama-C configuration.
[kernel] Warning: emitter emitter1: correctness parameter -s does not exist anymore. Ignored.
[kernel] Warning: emitter emitter2: correctness parameter -s2 does not exist anymore. Ignored.
[kernel] Warning: 13 states in saved file ignored. They are invalid in this Frama-C configuration.
[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
/* Generated by Frama-C */
int f(void)
{
int __retres;
/*@ assert emitter2: ∀ ℤ x; x ≡ x; */
int y = 0;
y ++;
/*@ assert y ≡ 1; */
/*@ assert emitter2: ∀ ℤ x; x ≡ x; */
;
__retres = 0;
/*@ assert emitter2: ∀ ℤ x; x ≡ x; */
return __retres;
}
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