--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on December 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Using Frama-C for Analyzing Linux Kernel



The following program shows the same behavior:

struct paravirt_callee_save {
  void *func;
};

struct pv_mmu_ops {
  struct paravirt_callee_save make_pte;
};

extern struct pv_mmu_ops pv_mmu_ops;

int main() {
   pv_mmu_ops.make_pte.func;
}

We'll take a look at it to see if Frama-C is being too strict.

On a side note, for future code posting, using another website such as 
Github Gist might be helpful. Ubuntu pastebin requires a login just to 
be able to download the text-only version...


On 01/12/2016 03:15, Nima Mohammadi wrote:
> Installed Silicium-rc1, but I still get the same error message.
> This is the preprocessed source ext2.mod.i, if you're interested: 
> http://paste.ubuntu.com/23560908/
>
> On Wed, Nov 30, 2016 at 12:58 PM, Gergö Barany <gergo.barany at cea.fr 
> <mailto:gergo.barany at cea.fr>> wrote:
>
>     On 29/11/16 21:11, Nima Mohammadi wrote:
>
>         ../.././arch/x86/include/asm/paravirt.h:407,86:[kernel] failure:
>         typeOffset: Field func on a non-compound type 'void *'
>
>
>     This looks strange. You could see if it's a bug in your version of
>     Frama-C that's fixed in the Silicium/Silicon release snapshot at
>     https://github.com/Frama-C/Frama-C-snapshot/releases
>     <https://github.com/Frama-C/Frama-C-snapshot/releases>
>
>     If not, it's probably impossible to say much more without the
>     preprocessed source you are trying to parse.
>
>     _______________________________________________
>     Frama-c-discuss mailing list
>     Frama-c-discuss at lists.gforge.inria.fr
>     <mailto:Frama-c-discuss at lists.gforge.inria.fr>
>     http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
>     <http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss>
>
>
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss

-- 
André Maroneze
Ingénieur-chercheur CEA/LIST
Laboratoire Sûreté et Sécurité des Logiciels

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20161201/42a03294/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 3797 bytes
Desc: S/MIME Cryptographic Signature
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20161201/42a03294/attachment.bin>