GitLab

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

---

Id	Project	Category	View	Due Date	Updated
ID0000188	Frama-C	Plug-in > slicing	public	2009-07-14	2009-07-15

Reporter	lukaszc	Assigned To	Anne	Resolution	won't fix
Priority	normal	Severity	major	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	-	Target Version	-	Fixed in Version	-

Description :

• jessie accepts this code and properly infers based on it, the slicing plug-in on the other hand indicates an error in the annotations

---

test.c

#include "test.h"

/@ @ requires y == CONS_FROM_TEST_H_DEFINED_USING_DEFINE; @ ensures @ \result == 2y; @/ int x(int y, int z) { /@ slice pragma ctrl; / //@ assert y == 1; //@ assert y + z == 3; return 2y*z1(); }

int main() { x(1,2); return 0; }

int z1() { return 1; }

test.h

#define CONS_FROM_TEST_H_DEFINED_USING_DEFINE 1