microsoft Armada issues

microsoft / Armada

Armada is a tool for writing, and proving correct, high-performance concurrent programs.

Other

137 stars 19 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Bump to nightly F* version

#35 gebner closed 7 months ago
6
adding binary expression to CreateLvalue

#34 MadeByMars closed 2 years ago
1
Grammar railroad diagram

#33 mingodad opened 3 years ago
1
Problem with C generation

#32 MadeByMars closed 2 years ago
0
Make compatible with Dafny 3.1.0

#31 jaylorch closed 3 years ago
0
remove check for multiple return arguments

#30 LukeXuan closed 3 years ago
1
Fix Shared-memory access counting

#29 LukeXuan closed 3 years ago
1
Return more than one value in concrete level

#28 MadeByMars closed 3 years ago
0
Forbid non-extern atomic methods in concrete levels

#27 jaylorch closed 3 years ago
0
Disallow arguments to return statements

#26 jaylorch closed 3 years ago
0
Check for pointer type validity

#25 jaylorch closed 3 years ago
0
Can't subtract integer from pointer into array

#24 jaylorch closed 3 years ago
0
Can't subtract pointers into same array

#23 jaylorch opened 3 years ago
0
Taking address of array causes crash

#22 jaylorch closed 3 years ago
0
Concrete levels can include non-external atomic methods

#21 jaylorch closed 3 years ago
0
Assume at end of if clause attaches to subsequent statement

#20 jaylorch opened 3 years ago
0
Empty statement not supported

#19 jaylorch opened 3 years ago
0
Concrete-level checker unnecessarily rejects return of multiple values

#18 jaylorch opened 3 years ago
0
Concrete levels can atomically return multiple shared locations

#17 jaylorch closed 3 years ago
0
Set up CI

#16 upamanyus opened 3 years ago
0
Regression test framework doesn't support negative examples

#15 jaylorch opened 3 years ago
0
Shared-memory access counting too conservative

#14 jaylorch closed 3 years ago
1
Invariant proofs split across files

#13 jaylorch opened 3 years ago
0
No support for thread-local storage

#12 jaylorch opened 3 years ago
0
Can't subtract pointers into the same array

#11 jaylorch opened 3 years ago
0
Generated files hard to distinguish from developer-written ones

#10 jaylorch opened 3 years ago
0
Pointers to non-heap types don't cause errors

#9 jaylorch closed 3 years ago
0
Customizations are per-lemma, not per-instruction

#8 jaylorch opened 3 years ago
0
Can't express well-formedness of an expression

#7 jaylorch opened 3 years ago
0
Can't customize a lemma by removing preconditions

#6 jaylorch opened 3 years ago
0
Can't specify inductive invariant sets

#5 jaylorch opened 3 years ago
0
Some emitted proof elements aren't needed

#4 jaylorch opened 3 years ago
0
dafny version

#3 jyizheng closed 4 years ago
9
Overview should mention that the target is standard C (ClightTSO)

#2 MaxBarraclough closed 4 years ago
1
adding some documentation / samples would be cool

#1 lizelive closed 4 years ago
0