Rafael Sá Menezes

As a partial requirement of https://github.com/esbmc/esbmc/pull/827#issuecomment-1199631426 This PR: 1. Creates the ssa_step_algorithm 2. Turns the slicer algorithms into ssa_step_algorithm 3. Adds a list of ssa_step_algorithms into bmct

SSA caching

9

This PR is a basis for the full caching framework. This adds: 1. SSA algorithms, which work similarly to the goto algorithms. This will help develop "passes" over SSA 2....

I am opening this as a draft for more discussion. @mikhailramalho has suggested me to look into the `incomplete_array` from CBMC. It seems that they actually removed it and use...

I'm just getting two crashes with the latest master, may I ask if you can take a look? It's on `vector_gcc_literal_shufflevector_3_false` and `vector_gcc_literal_shufflevector_3_true` when running with `--no-simplify --incremental-bmc`: ``` esbmc...

Extern symbols linking

1

Note: This is an incorrect approach for this! I am opening this as a PR so I can properly fix at ucode branch. Right now the PR is adding external...

ESBMC intrinsic library

2

We need a shared header to be used by users. This header should contain all ESBMC instructions that one might need for verifying its programs. - Depends on #641

Assert with dynamic strings don't work

2

Every assert that are using dynamic strings: ```c assert(0 && oss.str().c_str()); ``` I think that we should: 1. Replace them with the default_msg.error 2. Make msg.error abort Edit: List of...