Re: Please block chumley from building package cbmc
On Mon, Feb 16, 2015 at 11:40:33AM +0100, John Paul Adrian Glaubitz wrote:
> On 02/16/2015 09:14 AM, Michael Tautschnig wrote:
> >Would it be possible to blacklist cbmc on the host chumley?
> ^^^^^^^
> Looks like Christian hasn't fixed his buildd configuration and
> make sure the name used here is actually "crest" and not
> "chumley" :).
No, its somehow in the mail configuration, which I did not understand yet.
The mail is not going through chumley anymore, actually that server if off
since a while, so I don't know where the webpages pick up this name.
Anyhow, why is it inconsistent? The build has failed due to some tests:
Tests failed
2 of 342 tests failed, 21 tests skipped
Failed test: Function_Pointer7
CBMC version 5.0 32-bit linux
Parsing main.c
Converting
Type-checking main
file main.c line 22 function main: warning: conversion from `struct dev
(*)[4]' to `struct dev *': incompatible pointer types
file main.c line 26 function main: function `assert' is not declared
Generating GOTO Program
Adding CPROVER library
Function Pointer Removal
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
size of program expression: 47 steps
simple slicing removed 0 assignments
Generated 1 VCC(s), 0 remaining after simplification
VERIFICATION SUCCESSFUL
SIGNAL=0
Failed test: Struct_Initialization4
CBMC version 5.0 32-bit linux
Parsing main.c
Converting
Type-checking main
Generating GOTO Program
Adding CPROVER library
Function Pointer Removal
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
size of program expression: 44 steps
simple slicing removed 0 assignments
Generated 0 VCC(s), 0 remaining after simplification
VERIFICATION SUCCESSFUL
SIGNAL=0
I would not know how to blacklist one package one a buildd, but I guess it
will not pick it up again in the near future.
Christian
Reply to: