assigns nothing ?
ID0000617: This issue was created automatically from Mantis Issue 617. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000617 | Frama-C | Plug-in > jessie | public | 2010-10-26 | 2010-11-17 |
| Reporter | jnarboux | Assigned To | cmarche | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Boron-20100401 | Target Version | - | Fixed in Version | - |
Description :
Hi,
Using the following example:
/*@ ensures \result == 1; assigns \nothing; */
int foo() { int v[9]; v[0] =1; return 1; }
I get:
[kernel] preprocessing with "gcc -C -E -I. -dD bug.c" [jessie] Starting Jessie translation [jessie] Producing Jessie files in subdir bug.jessie [jessie] File bug.jessie/bug.jc written. [jessie] File bug.jessie/bug.cloc written. [jessie] Calling Jessie tool in subdir bug.jessie Generating Why function foo [jessie] Calling VCs generator. gwhy-bin [...] why/bug.why Computation of VCs... File "why/bug.why", line 392, characters 20-42: Unbound variable int_P_v_1_alloc_table make: *** [bug.stat] Erreur 1
is it normal ? if I remove the assign nothing it works.
Julien Narboux