-
Notifications
You must be signed in to change notification settings - Fork 31
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Update apalache integration test for compile
We now test that identifiers are sanitized, that imports and instances are resolved as expected, and that the unit is represented correctly.
- Loading branch information
Shon Feder
committed
Mar 14, 2024
1 parent
2c03d46
commit a742359
Showing
2 changed files
with
61 additions
and
15 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,35 @@ | ||
module ModuleToInstantiate { | ||
const C: int | ||
|
||
val instantiatedValue = C | ||
} | ||
|
||
module ModuleToImport { | ||
val importedValue = 0 | ||
} | ||
|
||
module ApalacheCompilation { | ||
// Tests whether we can compile imports | ||
import ModuleToImport.* | ||
|
||
// Tests whether we can compile instantiations | ||
import ModuleToInstantiate(C = 0).* | ||
|
||
var x: int | ||
|
||
type T = | ||
| A // Test whether we represent the unit correctly | ||
| B(int) | ||
|
||
// Tests whether we will sanitize identifiers | ||
def foo::bar(__123) = __123 | ||
|
||
// TODO: Tests that we remove primes from assignments in the init functino | ||
action init = { | ||
x' = importedValue + instantiatedValue | ||
} | ||
|
||
action step = x' = x + 1 | ||
|
||
def inv = x >= 0 | ||
} |