generated from amazon-archives/__template_Apache-2.0
-
Notifications
You must be signed in to change notification settings - Fork 136
Closed
Labels
[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.[E] User ExperienceAn UX enhancement for an existing feature. Including deprecation of an existing one.An UX enhancement for an existing feature. Including deprecation of an existing one.
Description
I tried verifying any code with either cargo kani or kani
using the following command line invocation:
cd $KANI_PROJECT/tests/kani/Assume
kani --quiet main.rs
with Kani version: 0.15.0
I expected to see this happen: No output should be printed.
Instead, Kani printed some CBMC messages.
$ kani --quiet main.rs
CBMC 5.70.0 (cbmc-5.70.0)
CBMC version 5.70.0 (cbmc-5.70.0) 64-bit x86_64 linux
Reading GOTO program from file main.for-check.out
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 16 object bits, 48 offset bits (user-specified)
Starting Bounded Model Checking
Runtime Symex: 0.000729304s
size of program expression: 46 steps
simple slicing removed 6 assignments
Generated 2 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 1.9209e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.000100889s
Running propositional reduction
Post-processing
Runtime Post-process: 3.471e-05s
Solving with MiniSAT 2.2.1 with simplifier
29 variables, 33 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 9.2524e-05s
Runtime decision procedure: 0.000229223s
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.[E] User ExperienceAn UX enhancement for an existing feature. Including deprecation of an existing one.An UX enhancement for an existing feature. Including deprecation of an existing one.