Si la valeur de retour est toujours dans d0, déclare kernel_LibsExec() comme retournant un entier 32 bits, que tu pourras caster comme tu veux ensuite.
Si ça ne suffit pas, tu peux t'en sortir en définissant un pointeur de fonction avec le type de retour kivabien, tu le fais pointer vers kernel_LibsExec() (via un cast, sinon le compilo va râler), et tu appelles la fonction à travers le pointeur. Mais c'est passablement lourd
(à vrai dire, il doit y avoir moyen de caster directement la fonction sans devoir utiliser de variable pointeur intermédiaire, mais vue la syntaxe ignoble du C pour les pointeurs de fonction, c'est à tes risques et périls ^^)