Skip to content

Commit

Permalink
Merge #1101
Browse files Browse the repository at this point in the history
1101: Update viper to 2022-07-21-0735 r=Aurel300 a=zgrannan

This update is required to support an optimization to the enum encoding (https://github.com/viperproject/prusti-dev/tree/enum_body_optimization).

Co-authored-by: Zack Grannan <zgrannan@protonmail.com>
  • Loading branch information
bors[bot] and zgrannan committed Jul 28, 2022
2 parents 9eb1c8e + c43ee3f commit a78a76d
Show file tree
Hide file tree
Showing 2 changed files with 4 additions and 3 deletions.
2 changes: 1 addition & 1 deletion viper-toolchain
Original file line number Diff line number Diff line change
@@ -1 +1 @@
v-2022-07-01-0736
v-2022-07-21-0735
5 changes: 3 additions & 2 deletions viper/src/silicon_counterexample.rs
Original file line number Diff line number Diff line change
Expand Up @@ -63,7 +63,7 @@ pub enum ModelEntry {
LitInt(String),
LitFloat(String),
LitBool(bool),
LitPerm(f64),
LitPerm(String),
Ref(String, FxHashMap<String, ModelEntry>),
NullRef(String),
RecursiveRef(String),
Expand Down Expand Up @@ -222,7 +222,8 @@ fn unwrap_model_entry<'a>(
}
"viper.silicon.reporting.LitPermEntry" => {
let lit_perm_wrapper = silicon::reporting::LitPermEntry::with(env);
let value = jni.unwrap_result(lit_perm_wrapper.call_value(entry));
let value_scala = jni.unwrap_result(lit_perm_wrapper.call_value(entry));
let value = jni.to_string(value_scala);
Some(ModelEntry::LitPerm(value))
}
"viper.silicon.reporting.RefEntry" => {
Expand Down

0 comments on commit a78a76d

Please sign in to comment.