added a case to simplify1PermForDetVars to end lifetimes which are no… …

… longer determined

changed equal shapes to be parameterized by a length

added rules SImpl_IntroLLVMBlockNamedMods and SImpl_ElimLLVMBlockName… …

…dMods to introduce an eliminate just the modalities on named shapes

added a case to eliminate equality shapes on the left when trying to … …

…prove a recursive shape on the right

updated examples to use the new form of the equality shape

changed load instructions to always load whole multiples of bytes at … …

…a time; added a FIXME for only storing whole multiples of bytes

added a comment about how to better support sub-byte-sized fields in … …

…RustTypes

added a new lborrowed permission that combines a simplified version o… …

…f the lowned permission with the actual permissions that are borrowed

removed the lborrowed permission in favor of a simplified lowned perm… …

…ission, which has the same permissions on input and output

added a debug level 2, with more debugging info

changed isProvablePerm so we always prove simple lowned permissions f… …

…irst; also changed implLLVMFieldTryProveWordEq to not drop equality permissions

fixed the layout for Rust enum and struct arguments: when they are la… …

…id out as pointers to values, the return permissions need to give back the memory where they were as an empty memblock permission

added the mk_proj0_five_values example to test out struct types passe… …

…d by value to called functions

Skeleton of decider for option-like Rust types

ChrisEPhifer committed Jan 13, 2022

Find a variant that carries data of type given by the type parameter;… …

… stop deciding option-like-ness if no such element is found

ChrisEPhifer committed Jan 13, 2022

Better name for function, finish implementation by confirming all oth… …

…er variants carry no data

ChrisEPhifer committed Jan 13, 2022

Cover struct-style fields for option-like enums

ChrisEPhifer committed Jan 14, 2022

If proving a tagged union shape where we know none of the tags match,… …

… fail right away

whoops, typo in error message

Merge branch 'heapster/more-rust-bugfixes' of github.com:GaloisInc/sa… …

…w-script into heapster/more-rust-bugfixes

added a special case to proveVarLLVMBlocks2 for proving a sequence sh… …

…ape with an unneeded empty shape

removed an unused variable warning; added a FIXME for proveVarLLVMBlo… …

…cks2

whoops, got the endianness wrong in bvSplit

bug fix: simplify1PermForDetVars also needs to end a lifetime when it… …

…s lowned permission contains undetermined vars, not just when the lifetime itself is not determined

added is_little_endian test case to c_data

added more rust_data examples

fixes for the rust_data example: fixed the definition of the List20 t… …

…ype; and added an assumption for the clone method for Box<List20<u64>>

Merge branch 'master' into heapster/more-rust-bugfixes

whoops, somehow these changes did not get committed in that last merge

Merge branch 'master' into heapster/more-rust-bugfixes