Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002454Frama-CPlug-in > wppublic2019-06-17 19:232019-06-19 09:47
Reporterjwaksbaum 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionno change required 
Platformi386OSDarwinOS Version18.6.0
Product Version 
Target VersionFixed in Version 
Summary0002454: Ambiguous path error using why3
DescriptionWhy3 errors on the generated goals produce by w3 on certain inputs with the following message:

Ambiguous path:
both /nix/store/nf4sbv0j6dc0grks7iplf9byv989mjg5-why3-0.88.3/share/why3/modules/Matrix.mlw
and /var/folders/2j/dbl_p0mj3rgd879z8nt7r4600000gp/T/wpdeac45.dir/typed/Matrix.why
Steps To ReproduceWhy3 errors on the generated goals produce by w3 on certain inputs with the following message:

Ambiguous path:
both /nix/store/nf4sbv0j6dc0grks7iplf9byv989mjg5-why3-0.88.3/share/why3/modules/Matrix.mlw
and /var/folders/2j/dbl_p0mj3rgd879z8nt7r4600000gp/T/wpdeac45.dir/typed/Matrix.why
TagsNo tags attached.
Attached Filesc file icon example.c [^] (239 bytes) 2019-06-17 19:23 [Show Content]

- Relationships

-  Notes
(0006790)
jwaksbaum (reporter)
2019-06-17 22:51

Sorry, the steps to reproduce should be running the following command on the attached example.c. Any prover that triggers why3 will work instead of z3.
$ frama-c -wp -wp-prover z3 example.c
(0006791)
jwaksbaum (reporter)
2019-06-17 22:57

I tested this on Ubuntu, and this issue doesn't occur because the files in share/why3/stdlib are lowercased, ie. matrix.mlw instead of Matrix.mlw, so it doesn't clash.
(0006792)
jwaksbaum (reporter)
2019-06-18 00:19

Actually, the files on Darwin are lowercase as well, so it's unclear why the conflict there and not on Ubuntu. At any rate, this is probably the result of a why3 issue, but Frama-C could also avoid the issue by changing the names of the generated files.
(0006793)
jwaksbaum (reporter)
2019-06-18 00:58

Apparently this is a known issue with Mac file systems handling case-sensitivity strangely, so I think it's on WP to generate a differently named file and not rely on the file system being case sensitive to differentiate between their file and the one in the standard library.
(0006794)
correnson (manager)
2019-06-18 10:58

Hi, thanks for the report.
I just tested the Frama-C 19-beta version under a Mac (and checked the file system is not case sensitive) on your example, but I can not reproduce the problem ; which precise version of Frama-C and Why-3 are you using ? Thanks !
(0006795)
jwaksbaum (reporter)
2019-06-18 18:38

I'm using Frama-C 18, and I've tried using Why-3 0.88.3 and 1.2.0.
(0006797)
jwaksbaum (reporter)
2019-06-19 00:19

I can confirm that with Frama-C 19-beta2 and Why3 1.2.0 this is no longer an issue.
(0006799)
correnson (manager)
2019-06-19 09:47

Thanks for reporting !
L.

- Issue History
Date Modified Username Field Change
2019-06-17 19:23 jwaksbaum New Issue
2019-06-17 19:23 jwaksbaum Status new => assigned
2019-06-17 19:23 jwaksbaum Assigned To => correnson
2019-06-17 19:23 jwaksbaum File Added: example.c
2019-06-17 22:51 jwaksbaum Note Added: 0006790
2019-06-17 22:57 jwaksbaum Note Added: 0006791
2019-06-18 00:19 jwaksbaum Note Added: 0006792
2019-06-18 00:58 jwaksbaum Note Added: 0006793
2019-06-18 10:58 correnson Note Added: 0006794
2019-06-18 18:38 jwaksbaum Note Added: 0006795
2019-06-19 00:19 jwaksbaum Note Added: 0006797
2019-06-19 09:46 correnson Note Added: 0006798
2019-06-19 09:46 correnson Status assigned => closed
2019-06-19 09:46 correnson Resolution open => no change required
2019-06-19 09:47 correnson Note Added: 0006799
2019-06-19 09:47 correnson Note Deleted: 0006798


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker