qutorial
qutorial
Dear all, this issue stays not fixed, and influences ownCloud client, as far as I understand from this bug discussion: https://github.com/owncloud/client/issues/3336#issuecomment-111465247 Is there a way I could help you to...
https://github.com/qutorial/hoststool This fork generates configuration for dnsmasq. Using it you could block domains and subdomains as well. Maybe this would be a working solution for you? Description could be found...
Results saved in: /Users/fortiss/mbeddr/mbeddr.github/code/applications/HeartBleed/solutions/analyses_results/HearBleedImpl/Model1/xmlCBMCRawOutput/HearBleedImpl.Model1_nightly.html java.lang.NullPointerException at com.mbeddr.analyses.cbmc.rt.run.HTMLResultsSaver$1.run(HTMLResultsSaver.java:66) at jetbrains.mps.ide.smodel.WorkbenchModelAccess$2.run(WorkbenchModelAccess.java:116) at com.intellij.openapi.application.impl.ApplicationImpl.runReadAction(ApplicationImpl.java:911) at jetbrains.mps.ide.smodel.WorkbenchModelAccess.runReadAction(WorkbenchModelAccess.java:111) at com.mbeddr.analyses.cbmc.rt.run.HTMLResultsSaver.generateHTMLPage(HTMLResultsSaver.java:63) at com.mbeddr.analyses.cbmc.rt.run.AnalysisConfigurationAnalyzer.doSaveResults(AnalysisConfigurationAnalyzer.java:161) at com.mbeddr.analyses.cbmc.rt.run.AnalysisConfigurationAnalyzer.doInBackground(AnalysisConfigurationAnalyzer.java:100) at com.mbeddr.analyses.cbmc.rt.run.AnalysisConfigurationAnalyzer.doInBackground(AnalysisConfigurationAnalyzer.java:1) at javax.swing.SwingWorker$1.call(SwingWorker.java:277) at java.util.concurrent.FutureTask$Sync.innerRun(FutureTask.java:303) at java.util.concurrent.FutureTask.run(FutureTask.java:138) at javax.swing.SwingWorker.run(SwingWorker.java:316) at...
Cbmc works fine on it, reporting a problem cbmc HeartBleed.c --bounds-check --pointer-check --function HeartBleed_verification --unwind 30
Continuing investigation: 1) On Linux and Windows: This is wrong to have 36 claims. They have to be 18. It probably counts from two functions, HeartBleed_verification and HeartBleed_verificationFixed, whereas only...
On mac a total of 24 claims is generated by CBMC, only 12 are shown by mbeddr
Ok, so it is in the filter claims where things are getting filtered out wrongly. Why to filter by the call graph, when cbmc accepts the --function property?
I brought back the formerly filtered out __built_in CBMC checks. But it still works differently on MAC, producing just 24 claims. None of them fails (one has to).
Okay. The memcpy() related bug is classified as an _arithmetic overflow_ problem by CBMC on Mac, instead of a pointer dereference :( To reproduce, just get the master, and run...