GitLab

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

---

Id	Project	Category	View	Due Date	Updated
ID0000473	Frama-C	Plug-in > jessie	public	2010-05-10	2010-10-14

Reporter	signoles	Assigned To	cmarche	Resolution	fixed
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Boron-20100401	Target Version	-	Fixed in Version	-

Description :

Jessie fails to generate the Why file corresponding to this trivial erroneous program:

===== void main(void) { int x = 1 / 0; }

$ frama-c -jessie a.c [kernel] preprocessing with "gcc -C -E -I. -dD a.c" [jessie] Starting Jessie translation [jessie] Producing Jessie files in subdir a.jessie [jessie] File a.jessie/a.jc written. [jessie] File a.jessie/a.cloc written. [jessie] Calling Jessie tool in subdir a.jessie Generating Why function main Uncaught exception: Failure("create_ratio infinite or undefined rational number") [jessie] user error: Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs a.cloc a.jc