tests/src/hashmap_main.rs


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

//@ charon-args=--opaque=hashmap_utils
//@ aeneas-args=-state -split-files
//@ [coq] aeneas-args=-use-fuel
//@ [fstar] aeneas-args=-decreases-clauses -template-clauses
// Possible to add `--no-code-duplication` if we use the optimized MIR
// TODO: reactivate -test-trans-units
mod hashmap;
mod hashmap_utils;

use crate::hashmap::*;
use crate::hashmap_utils::*;

pub fn insert_on_disk(key: Key, value: u64) {
    // Deserialize
    let mut hm = deserialize();
    // Update
    hm.insert(key, value);
    // Serialize
    serialize(hm);
}

pub fn main() {}