überSpark: Add frama-c and uberspark verification bridge with uberspark verification bridge plugin infrastructure

This task will add the following capabilities

  • Frama-c v20.0 verification bridge
  • überSpark verification bridge (based on Frama-c v20.0)
  • überSpark verification bridge plugin infrastructure

Linked PRs:

Merges:

Yo @Cap and/or @yeeb ,

Can you give this a quick whirl on your side:

  1. make clean, make and make install
  2. make within src-nextgen/coss-examples/hello-mul/ucoss-src. You will need to create the generic-platform staging environment using uberspark staging create generic-platform before issuing make here.

I can merge once you confirm the aforementioned tests pass on your side.

Thanks!

Getting an error after checking out the PR:

Populating namespace within: /home/uberspark/uberspark/_install...
cp -rf /home/uberspark/uberspark/src-nextgen/bridges/* /home/uberspark/uberspark/_install/bridges/
cp -f /home/uberspark/uberspark/src-nextgen/tools/vbridge-plugin/top/* /home/uberspark/uberspark/_install/tools/vbridge-plugin/.
cp: cannot stat '/home/uberspark/uberspark/src-nextgen/tools/vbridge-plugin/top/*': No such file or directory
make: *** [install.mk:57: install_populateamespace] Error 1
make: Leaving directory '/home/uberspark/uberspark/build-trusses'
Makefile:197: recipe for target 'install' failed
make: *** [install] Error 2

That is weird!

Can you post the ls -lR output within your: /home/uberspark/uberspark/src-nextgen/tools/vbridge-plugin/?

Also, perhaps your full build log might be useful too; am not sure if the vbridge-plugin build is succeeding…

I’m getting the same error. I don’t have a /home/uberspark directory.

@Cap and @yeeb,

Can both of you post your development platform details and full build logs please? This might help in figuring out the cause of this issue. Thanks!

Development platform:
Ubuntu 16.04 VM (using virtual box)

  • Linux 4.15.0-118

build log: out.txt (11.8 KB)

Did you follow the steps:

  1. make clean
  2. make
  3. make install

?

Your build log seems incomplete and does not contain the vbridge-plugin install target output…

yes. make clean and make completed successfully. so the build log was just for re-running make install

Can I get the make log?

log for make attached. make_out.txt (82.7 KB)

Aight. Looks like this was an error in the top-level Makefile orchestration. I pushed a potential fix to the PR. Can you pull and retest? Thanks!

Using the latest changset, I can successfully make install and make completes successfully, reporting built hello_mul successfully!

Ok great. Will proceed to merge this then. Thanks @cap!

Yep latest commit fixed it for me too!
built hello_mul successfully!

PR merged; OP updated. Closing task topic. Thanks @yeeb and @Cap for the tests!