GitLab

ID0000659: This issue was created automatically from Mantis Issue 659. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0000659	Frama-C	Plug-in > wp	public	2011-01-04	2011-01-31

Reporter	monate	Assigned To	dargaye	Resolution	fixed
Priority	normal	Severity	major	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Carbon-20101202-beta2	Target Version	Frama-C Carbon-20110201	Fixed in Version	-

Description :

On the following code :

/@ requires x != 0 ; behavior small_x: assumes x <= 256; ensures \result == 1; / int main(unsigned long long x) { if(( x & 0xffffffff00000000ll) == 0) { /@ assert (unsigned int)x != 0 ;/ return 1; }; return 0; }

I think everything should be provable. The generated POs are: Proof Obligation assert_1: Environment: Hoare_env1

• Assume hypothesis pre_1 Goal hoare_main_assert_1: forall x:int. is_in_format(uint64_format, x) -> (x <> 0) -> Then: ( (int_and(x,as_int(uint64_format,-4294967296)) = as_int(uint64_format,0)) -> (as_int(uint32_format,x) <> 0))

---

---

Function main with behavior small_x

Proof Obligation post_2: Environment: Hoare_env1

• Assume hypothesis pre_1
• Assume hypothesis pre_3 Goal hoare_main_small_x_post_2: forall x:int. is_in_format(uint64_format, x) -> (x <> 0) -> (x <= 256) -> Else: ( (int_and(x,as_int(uint64_format,-4294967296)) <> as_int(uint64_format,0)) -> false)

and I am almost sure they are not provable. The '-4294967296' looks like an undesired overflow during the WP translation.

Steps To Reproduce :

frama-c ll.c -wp -wp-model Hoare -wp-print