diff --git a/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle index 5a0fc4b056cc4d4e20fa1c9abef0dcf5cf6072f2..f7adb24d1e712d83b3051760e771795e5d040948 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle @@ -22,9 +22,9 @@ theory Compound (* use frama_c_wp.memory.Memory *) - function shift_sint32 (p:addr) (k:int) : addr = shift p k - function shiftfield_F1__list_next (p:addr) : addr = shift p 1 + + function shift_sint32 (p:addr) (k:int) : addr = shift p k end [wp:print-generated] theory WP diff --git a/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle index 56fce1fae014c63f99ea466d2d9e3981f3f7ea77..fe8a7c1947e4626c25d6564d6c9fc01af77c1fba 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle @@ -28,9 +28,9 @@ Require Import Qed. Require Import Memory. - Definition shift_sint32 (p : addr) (k : Z) : addr := (shift p k%Z). - Definition shiftfield_F1__list_next (p : addr) : addr := (shift p 1%Z). + + Definition shift_sint32 (p : addr) (k : Z) : addr := (shift p k%Z). [wp:print-generated] "WPOUT/typed/lemma_test_Coq.v" (* ---------------------------------------------------------- *)